A, B:Realizer.
((Rplus?(A)))
 ((Rplus?(B)))
 ((Rnone?(A)))
 ((Rnone?(B)))
 (R-base-domain(A) = R-base-domain(B)  (n:  base-domain-type(n)))
 (R-loc(A) = R-loc(B)  Id)
 (x:MaName. ((x  R-names(A)) & (x  R-names(B)))) 

latex

Definitions

P  Q, x:A. B(x), {T}, SQType(T), (i = j), p q, , True, if b then t else f fi , tt, ff, x. t(x), t  T, R-names(A), P & Q, MaName, R-loc(R), R-base-domain(R), base-domain-type(n), Rnone?(x1), Rplus?(x1), b, P  Q, x:A. B(x), P  Q, P  Q, t.2, t.1, False, x(s), Unit, A, Realizer, Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), Rpre(loc;ds;a;p;P), Rsends(ds;knd;T;l;dt;g), Reffect(loc;ds;knd;T;x;f), Rsframe(lnk;tag;L), Rframe(loc;T;x;L), Rinit(loc;T;x;v), left  right, Rnone(),

Lemmas

id-deq wf, remove-repeats wf, MaName wf, cons member, and functionality wrt iff, locl wf, append wf, fpf-trivial-subtype-top, fpf-domain wf, map wf, rcv wf, ldst wf, locknd wf, l member wf, LocKnd wf, Knd sq, IdLnk sq, lsrc wf, Id sq, pi2 wf, base-domain-type wf, pi1 wf, es realizer wf, false wf, true wf, not wf, bool wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, Knd wf, rationals wf, Id wf, unit wf